BDDs are effectively deployed in many EDA (Electronic Design Automation) tools, in particular in the area of formal verification. A plethora of public domain BDD packages is available on the web (see Meinel, Ch. Wagner, A., “WWW.BDD-PORTAL.ORG”, Proc. IEEE IWLS [Institute of Electrical and Electronics Engineers; International Workshop on Logic and Synthesis], pp. 341–348, 2000; [http colon backslash backslach www dot bdd-portal dot org]).
David Long (in D. E. Long, “The Design of a Cache-Friendly BDD Library”, Proc. ICCAD [International Conference on Computer Aided Design], pp. 639–645, 1998) introduces the notion of node-age and rearranges node allocation and garbage collection accordingly. Here, pointers are used to identify nodes. Problems are encountered when the memory allocator issues out-of-order blocks. The “reference objects” (analogous to what is termed further below as “handles”) use a hash table to ensure uniqueness (D. E. Long, private (email) communication, 1999) It will be shown further below that, in accordance with at least one embodiment of the present invention, no intermediate data structure is necessary; a slightly different garbage collection algorithm is used.
Other disadvantages have been observed in connection wit prior efforts. Long 1998, supra, does not address dynamic variable ordering. The BDDs as implemented in earlier versions of SMV (Symbolic Model Verifier) (see K. L. McMillan, Symbolic Model Checking, Kluwer, 1993), do not use node reference counts; a mark-sweep garbage collector is used. For variable reordering an algorithm by R. Rudell (R. Rudell, “Dynamic variable ordering for ordered binary decision diagrams”, Proc. ICCAD, pp. 42–47, 1993) is employed, but SMV does excessive BDD traversals to calculate accurate live node counts because no explicit reference counts are used. A package called ABCD (Biere, Armin, ABCD: a compact BDD library, http colon backslash backslash www dot inf dot erhz dot ch backslash personal backslash biere backslash projects backslash abed, 2000) focuses on compactness of representation (only 8 bytes per node) and uses indices to achieve this. It does not take advantage of the node order and does not offer dynamic variable ordering. Also its memory management is rather rigid.
In view of the foregoing, a need has been recognized in connection with overcoming the shortcomings and disadvantages presented by conventional arrangements.